#!/usr/bin/python

import optparse
import os
import subprocess

def runcommand(command):
  global log
  print "* Running " + command
  subprocess.call(command, shell=True, stdout=log, stderr=subprocess.STDOUT)
  
def dertablefile(pr,r):
  global outbase
  return outbase+"-"+pr+"-"+r+".pro"
  
def dertablecommand1(pr,r,outfile):
  return "swipl -G4g " + args[0] + " " + pr + " " + r + " < tomaths.pro > protocol.m && math -script code.m"

def dertablecommand2(pr,r,outfile):
  return "cp out " + outfile
  
def dertablecommand3(pr,r,outfile):
  return "swipl " + args[0] + " " + outfile + " " + pr + " " + r + " < internalce.pro >> " + outfile

def analysisfile(pr,r):
  global outbase
  return outbase+"-"+pr+"-"+r+".tex"
  
def analysiscommand(pr,r,infile,outfile):
  return "swipl " + infile + " " + pr + " " + r + " < analyse.pro > " + outfile


usage = "usage: %prog [options] file.pro"
p = optparse.OptionParser(usage=usage, version="$Date: 2013/02/06 14:10:21 $")
p.add_option("--outdir","-O",action="store",dest="outdir", help="Output directory (default: current directory)")
p.add_option("--outfile","-o",action="store",dest="outfile", help="Output file (single table/analysis mode)")
p.add_option("--table","-t",action="store",dest="prt", help="Compute derivation table for given protocol:role")
p.add_option("--analyse","-a",action="store",dest="pra", help="Perform linkability/detectability analysis for given protocol:role")
p.add_option("--makefile","-m",action="store_const",dest="makefile", const=True, help="Generate Makefile instead of performing analysis")
p.set_defaults(outdir="",outfile=False,prt=False,pra=False,makefile=False)
opts,args = p.parse_args()

if len(args)!= 1:
  p.print_help()
  exit(2)
  
if opts.outdir != "" and opts.outdir[-1] != "/": opts.outdir = opts.outdir + "/"

try:
  name,_,ext=os.path.basename(args[0]).rpartition('.')
  if ext!="pro": raise ValueError
except ValueError:
  print "*** ERROR: Input file should have \".pro\" extension"
  p.print_help()
  exit(2)

outbase = opts.outdir + name
logfile = outbase + ".log"

log = open(logfile, "w")

if opts.prt:
  try:
    pr,r=opts.prt.split(':') 
  except ValueError:
    print "*** ERROR: Argument to --table should be of the form protocol:role"
    p.print_help()
    exit(2)
  if not opts.outfile: opts.outfile=dertablefile(pr,r)
  runcommand(dertablecommand(pr,r,opts.outfile))
  exit(0)
  
if opts.pra:
  try:
    pr,r=opts.pra.split(':') 
  except ValueError:
    print "*** ERROR: Argument to --analyse should be of the form protocol:role"
    p.print_help()
    exit(2)
    
  infile = outbase+"-all.pro"
  if os.path.exists(infile):
    print "*** Using table file " + infile
  else:
    infile = args[0]
    
  if not opts.outfile: opts.outfile = analysisfile(pr,r)
  
  runcommand(analysiscommand(pr,r,infile,opts.outfile))
  exit(0)
  
 # find all protocols/roles
all = subprocess.check_output("swipl " + args[0] + " < printroles.pro", stderr=log, shell=True)
roles = map((lambda x: x.split(',')), all[2:-2].split('),('))

if opts.makefile:
  mfile = open("Makefile." + name, "w")
  
#  mfile.write("Makefile." + name + ": analyse " + args[0] + "\n")
#  mfile.write("\t./analyse " + args[0] + " -O " + opts.outdir + " -m\n\n")
  
  # generate makefile
  mfile.write(name + ": " + outbase + "-all.tex\n")
  mfile.write("\n")
  
  mfile.write(outbase + "-all.tex: " + " ".join(map(lambda x: analysisfile(x[0],x[1]),roles)) + " " + outbase + "-prims.tex" + "\n")
  #mfile.write("\trm -f " + outbase + "-all.tex" + "\n")
  mfile.write("\tcat " + outbase + "-prims.tex > " + outbase + "-all.tex" + "\n")
  for x in roles: mfile.write("\tcat " + analysisfile(x[0],x[1]) + " >> " + outbase + "-all.tex" + "\n")
  mfile.write("\n")
  
  mfile.write(outbase + "-prims.tex: " + args[0] + " primitives.pro printmessages.pro symbolic.pro\n")
  mfile.write("\tswipl " + args[0] + " < primitives.pro > " + outbase + "-prims.tex\n\n")
  
  for x in roles:
    mfile.write(analysisfile(x[0],x[1]) + ": " + outbase + "-all.pro analyse.pro printmessages.pro symbolic.pro" + "\n")
    mfile.write("\t" + analysiscommand(x[0],x[1],outbase + "-all.pro",analysisfile(x[0],x[1])) + " 2> " + logfile + "\n")
    mfile.write("\n")
  
  mfile.write(outbase + "-all.pro: " + " ".join(map(lambda x: dertablefile(x[0],x[1]),roles)) + "\n")
  mfile.write("\techo \":- include('" + args[0] + "').\" > " + outbase + "-all.pro" + "\n")
  mfile.write("\techo >> " + outbase + "-all.pro" + "\n")
  for x in roles: mfile.write("\tcat " + dertablefile(x[0],x[1]) + " >> " + outbase + "-all.pro" + "\n")
  mfile.write("\n")
  
  for x in roles:
    mfile.write(dertablefile(x[0],x[1]) + ": " + args[0] + " internalce.pro printmessages.pro symbolic.pro tomaths.pro constraints.pro code.m" + "\n")
    mfile.write("\t" + dertablecommand1(x[0],x[1],dertablefile(x[0],x[1])) + " 2> " + logfile + "\n")
    mfile.write("\t" + dertablecommand2(x[0],x[1],dertablefile(x[0],x[1])) + " 2> " + logfile + "\n")
    mfile.write("\t" + dertablecommand3(x[0],x[1],dertablefile(x[0],x[1])) + " 2> " + logfile + "\n")
    mfile.write("\n")
    
  mfile.write(name + "-clean: " + "\n")
  mfile.write("\trm -f " + outbase + "-prims.tex" + "\n")
  mfile.write("\trm -f " + outbase + ".log" + "\n")
  mfile.write("\trm -f " + outbase + "-all.tex" + "\n")
  for x in roles:
    mfile.write("\trm -f " + analysisfile(x[0],x[1]) + "\n")
  mfile.write("\trm -f " + outbase + "-all.pro" + "\n")
  for x in roles:
    mfile.write("\trm -f " + dertablefile(x[0],x[1]) + "\n")
  
  mfile.close()
  exit(0)
  
# compute derivation tables and write into combined file
allfilename = outbase + "-all.pro"
allfile = open(allfilename, "w")
allfile.write(":- include('" + args[0] + "').\n\n")
for [pr,r] in roles:
  runcommand(dertablecommand(pr,r,dertablefile(pr,r)))
  df = open(dertablefile(pr,r))
  allfile.write(df.read())
  df.close()    
allfile.close()

# analyse
allfile = open(outbase + "-all.tex", "w")
for [pr,r] in roles:
  runcommand(analysiscommand(pr,r,allfilename,analysisfile(pr,r)))
  af = open(analysisfile(pr,r))
  allfile.write(af.read())
  af.close()
allfile.close()
